import GlimpseOfLean.Library.Basic

open Function

/-
## 合取

在这个文件中，我们学习如何处理合取（"逻辑与"）操作符和存在量词。

在 Lean 中，两个命题 `P` 和 `Q` 的合取记为 `P ∧ Q`，读作"P 和 Q"。

我们可以像使用 `↔` 一样使用合取：
* 如果 `h : P ∧ Q`，那么 `h.1 : P` 且 `h.2 : Q`。
* 要证明 `P ∧ Q`，使用 `constructor` 策略。

此外，我们可以分解合取和等价关系。
* 如果 `h : P ∧ Q`，策略 `rcases h with ⟨hP, hQ⟩` 给出两个新假设 `hP : P` 和 `hQ : Q`。
* 如果 `h : P ↔ Q`，策略 `rcases h with ⟨hPQ, hQP⟩` 给出两个新假设 `hPQ : P → Q` 和 `hQP : Q → P`。
-/

example (p q r s : Prop) (h : p → r) (h' : q → s) : p ∧ q → r ∧ s := by
  intro hpq
  rcases hpq with ⟨hp, hq⟩
  constructor
  · exact h hp
  · exact h' hq

/- 也可以通过使用 `⟨`/`⟩` 括号收集两边来证明合取，而不使用 constructor 策略，因此上面的证明可以重写为。 -/

example (p q r s : Prop) (h : p → r) (h' : q → s) : p ∧ q → r ∧ s := by
  intro hpq
  exact ⟨h hpq.1, h' hpq.2⟩

/- 在下一个练习中你可以选择自己的风格。 -/

example (p q r : Prop) : (p → (q → r)) ↔ p ∧ q → r := by
  -- sorry
  constructor
  · intro h h'
    rcases h' with ⟨hp, hq⟩
    exact h hp hq
  · intro h hp hq
    apply h
    constructor
    · exact hp
    · exact hq
  -- sorry

/- 当然 Lean 不需要任何帮助来证明这种逻辑重言式。这是 `tauto` 策略的工作，它可以证明命题逻辑中的真命题。 -/
example (p q r : Prop) : (p → (q → r)) ↔ p ∧ q → r := by
  tauto

/- # 存在量词

为了证明 `∃ x, P x`，我们使用策略 `use x₀` 给出某个 `x₀`，然后证明 `P x₀`。这个 `x₀` 可以是局部上下文中的对象或者更复杂的表达式。在下面的例子中，`use` 之后要检查的性质根据定义为真，所以证明结束了。
-/
example : ∃ n : ℕ, 8 = 2*n := by
  use 4

/-
为了使用 `h : ∃ x, P x`，我们使用 `rcases` 策略来固定一个有效的 `x₀`。

这里 `h` 可以直接来自局部上下文，也可以是更复杂的表达式。
-/
example (n : ℕ) (h : ∃ k : ℕ, n = k + 1) : n > 0 := by
  -- 设 k₀ 使得 n = k₀ + 1。
  rcases h with ⟨k₀, hk₀⟩
  -- 现在只需证明 k₀ + 1 > 0。
  rw [hk₀]
  -- 而我们有关于此的引理
  exact Nat.succ_pos k₀

/-
接下来的练习使用 ℤ 中的整除性（注意 ∣ 符号不是 ASCII 符号）。

根据定义，`a ∣ b ↔ ∃ k, b = a*k`，所以你可以使用 `use` 策略来证明 `a ∣ b`。
-/

example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := by
  -- sorry
  rcases h₁ with ⟨k, hk⟩
  rcases h₂ with ⟨l, hl⟩
  use k*l
  calc
    c = b*l   := hl
    _ = (a*k)*l := by rw [hk]
    _ = a*(k*l) := by ring
  -- sorry


/-
我们现在可以开始组合量词，使用定义

  `Surjective (f : X → Y) := ∀ y, ∃ x, f x = y`
-/

example (f g : ℝ → ℝ) (h : Surjective (g ∘ f)) : Surjective g := by
  -- sorry
  intro y
  rcases h y with ⟨w, hw⟩
  use f w
  exact hw
  -- sorry

/- 这是关于 `∃` 和 `∧` 的文件的结尾。你学会了策略
* `rcases`
* `tauto`
* `use`

这是 `Basics` 文件夹的结尾。我们故意省略了逻辑或操作符和关于否定的所有内容，以便你能尽快进入实际的数学内容。你现在可以从 `Topics` 中选择一个文件。

关于选择的描述请参见 `03Forall` 的底部。
-/
